Inference at * 1 1 
Iof proof for Lemma inv image ind a:



1. T : Type
2. r : TT
3. S : Type
4. f : ST
5. WellFnd{i}(T;x,y.r(x,y))
6. P : S
7. j:S. (k:S. r(f(k),f(j))  P(k))  P(j)
8. n : S
  P(n) 

latex

 by ((% Switch quantification to T % 
Assert x:T, y:S. (f(y) = x)  P(y)) 
ACollapseTHEN (IfLabL

AC[`assertion`,((D 0) 
ACollapseTHENA ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 4:n
AC)) (first_tok :t) inil_term))) 
AC;`main`,((InstHyp [f(n);n] (-1)) 
ACollapseTHEN (
AC(Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n)) (first_tok :t) inil_term)))])) 

latex

AC1: 

AC1: 9. x : T
AC1:   y:S. (f(y) = x)  P(y)
AC.

Definitions

t  T, x:A. B(x), P  Q